There are many representations for program analysis or verification at the source code level. However, binary code also needs analysis. Binary analysis may determine the integrity of the binary and look for malicious code. Also, many developers only ship binaries and do not make their source code available to others. However, recipients of such binaries still may wish to verify the integrity of the binary code.